$\forall$$X$:Type\{j\}, ${\it Cmd}$:Type\{i\}, $x$:chain\_sys(${\it Cmd}$), ${\it input}$:(${\it Cmd}$$\rightarrow$$X$), ${\it update}$:(Id$\rightarrow$(${\it Cmd}$ List)$\rightarrow$$X$).
\\[0ex]chain\_sys\_ind($x$;${\it cmd}$.${\it input}$(${\it cmd}$);${\it from}$,${\it cmds}$.${\it update}$(${\it from}$,${\it cmds}$)) $\in$ $X$